Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
active(c) |
→ mark(f(g(c))) |
| 2: |
|
active(f(g(X))) |
→ mark(g(X)) |
| 3: |
|
proper(c) |
→ ok(c) |
| 4: |
|
proper(f(X)) |
→ f(proper(X)) |
| 5: |
|
proper(g(X)) |
→ g(proper(X)) |
| 6: |
|
f(ok(X)) |
→ ok(f(X)) |
| 7: |
|
g(ok(X)) |
→ ok(g(X)) |
| 8: |
|
top(mark(X)) |
→ top(proper(X)) |
| 9: |
|
top(ok(X)) |
→ top(active(X)) |
|
There are 12 dependency pairs:
|
| 10: |
|
ACTIVE(c) |
→ F(g(c)) |
| 11: |
|
ACTIVE(c) |
→ G(c) |
| 12: |
|
PROPER(f(X)) |
→ F(proper(X)) |
| 13: |
|
PROPER(f(X)) |
→ PROPER(X) |
| 14: |
|
PROPER(g(X)) |
→ G(proper(X)) |
| 15: |
|
PROPER(g(X)) |
→ PROPER(X) |
| 16: |
|
F(ok(X)) |
→ F(X) |
| 17: |
|
G(ok(X)) |
→ G(X) |
| 18: |
|
TOP(mark(X)) |
→ TOP(proper(X)) |
| 19: |
|
TOP(mark(X)) |
→ PROPER(X) |
| 20: |
|
TOP(ok(X)) |
→ TOP(active(X)) |
| 21: |
|
TOP(ok(X)) |
→ ACTIVE(X) |
|
The approximated dependency graph contains 4 SCCs:
{16},
{17},
{13,15}
and {18,20}.
-
Consider the SCC {16}.
There are no usable rules.
By taking the AF π with
π(F) = 1 together with
the lexicographic path order with
empty precedence,
rule 16
is strictly decreasing.
-
Consider the SCC {17}.
There are no usable rules.
By taking the AF π with
π(G) = 1 together with
the lexicographic path order with
empty precedence,
rule 17
is strictly decreasing.
-
Consider the SCC {13,15}.
There are no usable rules.
By taking the AF π with
π(f) = π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 13
is weakly decreasing and
rule 15
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {13}.
By taking the AF π with
π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 13
is strictly decreasing.
-
Consider the SCC {18,20}.
The usable rules are {1-7}.
By taking the AF π with
π(active) = π(ok) = π(proper) = π(TOP) = 1
and π(f) = π(g) = [ ] together with
the lexicographic path order with
precedence c ≻ f ≻ g
and f ≻ mark,
the rules in {3-7,20}
are weakly decreasing and
the rules in {1,2,18}
are strictly decreasing.
There is one new SCC.
-
Consider the SCC {20}.
The usable rules are {1,2,6,7}.
By taking the AF π with
π(f) = π(g) = π(TOP) = 1
and π(active) = π(mark) = π(ok) = [ ] together with
the lexicographic path order with
precedence ok ≻ active ≻ mark,
the rules in {6,7}
are weakly decreasing and
the rules in {1,2,20}
are strictly decreasing.
Hence the TRS is terminating.
Tyrolean Termination Tool (0.20 seconds)
--- May 3, 2006